* Step 1: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
filter(cons(X),0(),M) -> cons(0())
filter(cons(X),s(N),M) -> cons(X)
nats(N) -> cons(N)
sieve(cons(0())) -> cons(0())
sieve(cons(s(N))) -> cons(s(N))
zprimes() -> sieve(nats(s(s(0()))))
- Signature:
{filter/3,nats/1,sieve/1,zprimes/0} / {0/0,cons/1,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {filter,nats,sieve,zprimes} and constructors {0,cons,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
filter#(cons(X),0(),M) -> c_1()
filter#(cons(X),s(N),M) -> c_2()
nats#(N) -> c_3()
sieve#(cons(0())) -> c_4()
sieve#(cons(s(N))) -> c_5()
zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
filter#(cons(X),0(),M) -> c_1()
filter#(cons(X),s(N),M) -> c_2()
nats#(N) -> c_3()
sieve#(cons(0())) -> c_4()
sieve#(cons(s(N))) -> c_5()
zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
- Weak TRS:
filter(cons(X),0(),M) -> cons(0())
filter(cons(X),s(N),M) -> cons(X)
nats(N) -> cons(N)
sieve(cons(0())) -> cons(0())
sieve(cons(s(N))) -> cons(s(N))
zprimes() -> sieve(nats(s(s(0()))))
- Signature:
{filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/1,s/1,c_1/0,c_2/0
,c_3/0,c_4/0,c_5/0,c_6/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons
,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
nats(N) -> cons(N)
filter#(cons(X),0(),M) -> c_1()
filter#(cons(X),s(N),M) -> c_2()
nats#(N) -> c_3()
sieve#(cons(0())) -> c_4()
sieve#(cons(s(N))) -> c_5()
zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
* Step 3: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
filter#(cons(X),0(),M) -> c_1()
filter#(cons(X),s(N),M) -> c_2()
nats#(N) -> c_3()
sieve#(cons(0())) -> c_4()
sieve#(cons(s(N))) -> c_5()
zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
- Weak TRS:
nats(N) -> cons(N)
- Signature:
{filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/1,s/1,c_1/0,c_2/0
,c_3/0,c_4/0,c_5/0,c_6/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons
,s}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph
1:S:filter#(cons(X),0(),M) -> c_1()
2:S:filter#(cons(X),s(N),M) -> c_2()
3:S:nats#(N) -> c_3()
4:S:sieve#(cons(0())) -> c_4()
5:S:sieve#(cons(s(N))) -> c_5()
6:S:zprimes#() -> c_6(sieve#(nats(s(s(0())))),nats#(s(s(0()))))
-->_1 sieve#(cons(s(N))) -> c_5():5
-->_1 sieve#(cons(0())) -> c_4():4
-->_2 nats#(N) -> c_3():3
The dependency graph contains no loops, we remove all dependency pairs.
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
nats(N) -> cons(N)
- Signature:
{filter/3,nats/1,sieve/1,zprimes/0,filter#/3,nats#/1,sieve#/1,zprimes#/0} / {0/0,cons/1,s/1,c_1/0,c_2/0
,c_3/0,c_4/0,c_5/0,c_6/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {filter#,nats#,sieve#,zprimes#} and constructors {0,cons
,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(1))